$\forall$${\it es}$:ES, $i$:Id, $a$:Atom1. $i$ $>>$ $a$ $\in$ Prop